

LEMMA

tpp gives pp
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c515443 c515442)) v (pp c515443 c515442))


> hypdisj
=============================
Step 3

? (pp c515443 c515442)

1. (tpp c515443 c515442)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c515443 c515442)

1. (~ (pp c515443 c515442))
2. (tpp c515443 c515442)

> hyp


LEMMA

pp gives p
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c516495 c516494)) v (p c516495 c516494))


> hypdisj
=============================
Step 3

? (p c516495 c516494)

1. (pp c516495 c516494)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c516495 c516494)

1. (~ (p c516495 c516494))
2. (pp c516495 c516494)

> hyp


LEMMA

po gives overlap
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c518122 c518121)) v (o c518122 c518121))


> hypdisj
=============================
Step 3

? (o c518122 c518121)

1. (po c518122 c518121)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c518122 c518121)

1. (~ (o c518122 c518121))
2. (po c518122 c518121)

> hyp


LEMMA

po excludes p(z,y)
=============================
Step 1

? (all x (all y ((po x y) => (~ (p y x)))))


> revsk
=============================
Step 2

? ((~ (po c518126 c518125)) v (~ (p c518125 c518126)))


> hypdisj
=============================
Step 3

? (~ (p c518125 c518126))

1. (po c518126 c518125)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 4

? (po c518126 c518125)

1. (p c518125 c518126)
2. (po c518126 c518125)

> hyp


LEMMA

c splits into ec or overlap
=============================
Step 1

? (all x (all y ((c x y) => ((ec x y) v (o x y)))))


> revsk
=============================
Step 2

? ((~ (c c519235 c519234)) v ((ec c519235 c519234) v (o c519235 c519234)))


> hypdisj
=============================
Step 3

? (o c519235 c519234)

1. (~ (ec c519235 c519234))
2. (c c519235 c519234)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c519235 c519234)
|
|1. (~ (o c519235 c519234))
|2. (~ (ec c519235 c519234))
|3. (c c519235 c519234)
|
|> hyp
=============================
Step 5

? (~ (ec c519235 c519234))

1. (~ (o c519235 c519234))
2. (~ (ec c519235 c519234))
3. (c c519235 c519234)

> hyp


LEMMA

dc or c
=============================
Step 1

? (all x (all y ((dc x y) v (c x y))))


> revsk
=============================
Step 2

? ((dc c519698 c519697) v (c c519698 c519697))


> hypdisj
=============================
Step 3

? (c c519698 c519697)

1. (~ (dc c519698 c519697))

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c519698 c519697))

1. (~ (c c519698 c519697))
2. (~ (dc c519698 c519697))

> hyp


LEMMA

pp refines to tpp or ntpp
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c522099 c522098)) v ((tpp c522099 c522098) v (ntpp c522099 c522098)))


> hypdisj
=============================
Step 3

? (ntpp c522099 c522098)

1. (~ (tpp c522099 c522098))
2. (pp c522099 c522098)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f519736 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c522099 c522098)
|
|1. (~ (ntpp c522099 c522098))
|2. (~ (tpp c522099 c522098))
|3. (pp c522099 c522098)
|
|> hyp
=============================
Step 5

? (~ (ec (f519736 c522099 c522098 Var32) c522099))

1. (~ (ntpp c522099 c522098))
2. (~ (tpp c522099 c522098))
3. (pp c522099 c522098)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c522099 Var36)
||
||1. (ec (f519736 c522099 c522098 Var32) c522099)
||2. (~ (ntpp c522099 c522098))
||3. (~ (tpp c522099 c522098))
||4. (pp c522099 c522098)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f519736 c522099 c522098 Var32) c522098)
|
|1. (ec (f519736 c522099 c522098 Var32) c522099)
|2. (~ (ntpp c522099 c522098))
|3. (~ (tpp c522099 c522098))
|4. (pp c522099 c522098)
|
|> ((ec (f519736 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c522099 c522098))
||
||1. (~ (ec (f519736 c522099 c522098 Var32) c522098))
||2. (ec (f519736 c522099 c522098 Var32) c522099)
||3. (~ (ntpp c522099 c522098))
||4. (~ (tpp c522099 c522098))
||5. (pp c522099 c522098)
||
||> hyp
|=============================
|Step 9
|
|? (pp c522099 c522098)
|
|1. (~ (ec (f519736 c522099 c522098 Var32) c522098))
|2. (ec (f519736 c522099 c522098 Var32) c522099)
|3. (~ (ntpp c522099 c522098))
|4. (~ (tpp c522099 c522098))
|5. (pp c522099 c522098)
|
|> hyp
=============================
Step 10

? (~ (tpp c522099 c522098))

1. (ec (f519736 c522099 c522098 Var32) c522099)
2. (~ (ntpp c522099 c522098))
3. (~ (tpp c522099 c522098))
4. (pp c522099 c522098)

> hyp


LEMMA

under tpp(x,y) and po(y,z), overlap xz refines to po or pp
=============================
Step 1

? (all x (all y (all z ((((tpp x y) & (po y z)) & (o x z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? ((((~ (tpp c524730 c524729)) v (~ (po c524729 c524728))) v (~ (o c524730 c524728))) v ((po c524730 c524728) v (pp c524730 c524728)))


> hypdisj
=============================
Step 3

? (pp c524730 c524728)

1. (~ (po c524730 c524728))
2. (o c524730 c524728)
3. (po c524729 c524728)
4. (tpp c524730 c524729)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c524730 c524728)
|
|1. (~ (pp c524730 c524728))
|2. (~ (po c524730 c524728))
|3. (o c524730 c524728)
|4. (po c524729 c524728)
|5. (tpp c524730 c524729)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c524728 c524730)
||
||1. (~ (p c524730 c524728))
||2. (~ (pp c524730 c524728))
||3. (~ (po c524730 c524728))
||4. (o c524730 c524728)
||5. (po c524729 c524728)
||6. (tpp c524730 c524729)
||
||> ((p Z X) <-- (~ (c (f522113 Z X Y) Z)))
||=============================
||Step 6
||
||? (~ (c (f522113 c524728 c524730 Var100) c524728))
||
||1. (~ (p c524728 c524730))
||2. (~ (p c524730 c524728))
||3. (~ (pp c524730 c524728))
||4. (~ (po c524730 c524728))
||5. (o c524730 c524728)
||6. (po c524729 c524728)
||7. (tpp c524730 c524729)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 7
|||
|||? (p c524728 Var103)
|||
|||1. (c (f522113 c524728 c524730 Var100) c524728)
|||2. (~ (p c524728 c524730))
|||3. (~ (p c524730 c524728))
|||4. (~ (pp c524730 c524728))
|||5. (~ (po c524730 c524728))
|||6. (o c524730 c524728)
|||7. (po c524729 c524728)
|||8. (tpp c524730 c524729)
|||
|||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (o Var103 c524728)
|||||
|||||1. (~ (p c524728 Var103))
|||||2. (c (f522113 c524728 c524730 Var100) c524728)
|||||3. (~ (p c524728 c524730))
|||||4. (~ (p c524730 c524728))
|||||5. (~ (pp c524730 c524728))
|||||6. (~ (po c524730 c524728))
|||||7. (o c524730 c524728)
|||||8. (po c524729 c524728)
|||||9. (tpp c524730 c524729)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (p c524730 c524728))
||||
||||1. (~ (p c524728 c524730))
||||2. (c (f522113 c524728 c524730 Var100) c524728)
||||3. (~ (p c524728 c524730))
||||4. (~ (p c524730 c524728))
||||5. (~ (pp c524730 c524728))
||||6. (~ (po c524730 c524728))
||||7. (o c524730 c524728)
||||8. (po c524729 c524728)
||||9. (tpp c524730 c524729)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (po c524730 c524728))
|||
|||1. (~ (p c524728 c524730))
|||2. (c (f522113 c524728 c524730 Var100) c524728)
|||3. (~ (p c524728 c524730))
|||4. (~ (p c524730 c524728))
|||5. (~ (pp c524730 c524728))
|||6. (~ (po c524730 c524728))
|||7. (o c524730 c524728)
|||8. (po c524729 c524728)
|||9. (tpp c524730 c524729)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (c (f522113 c524728 c524730 Var100) c524730))
||
||1. (c (f522113 c524728 c524730 Var100) c524728)
||2. (~ (p c524728 c524730))
||3. (~ (p c524730 c524728))
||4. (~ (pp c524730 c524728))
||5. (~ (po c524730 c524728))
||6. (o c524730 c524728)
||7. (po c524729 c524728)
||8. (tpp c524730 c524729)
||
||> ((~ (c (f522113 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 12
||
||? (~ (p c524728 c524730))
||
||1. (c (f522113 c524728 c524730 Var100) c524730)
||2. (c (f522113 c524728 c524730 Var100) c524728)
||3. (~ (p c524728 c524730))
||4. (~ (p c524730 c524728))
||5. (~ (pp c524730 c524728))
||6. (~ (po c524730 c524728))
||7. (o c524730 c524728)
||8. (po c524729 c524728)
||9. (tpp c524730 c524729)
||
||> hyp
|=============================
|Step 13
|
|? (~ (pp c524728 c524730))
|
|1. (~ (p c524730 c524728))
|2. (~ (pp c524730 c524728))
|3. (~ (po c524730 c524728))
|4. (o c524730 c524728)
|5. (po c524729 c524728)
|6. (tpp c524730 c524729)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 14
|
|? (~ (p c524728 c524730))
|
|1. (pp c524728 c524730)
|2. (~ (p c524730 c524728))
|3. (~ (pp c524730 c524728))
|4. (~ (po c524730 c524728))
|5. (o c524730 c524728)
|6. (po c524729 c524728)
|7. (tpp c524730 c524729)
|
|> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
||=============================
||Step 15
||
||? (c (f522113 c524728 Var120 Var121) c524728)
||
||1. (p c524728 c524730)
||2. (pp c524728 c524730)
||3. (~ (p c524730 c524728))
||4. (~ (pp c524730 c524728))
||5. (~ (po c524730 c524728))
||6. (o c524730 c524728)
||7. (po c524729 c524728)
||8. (tpp c524730 c524729)
||
||> ((c (f522113 Y Z X) Y) <-- (~ (p Y Z)))
||=============================
||Step 16
||
||? (~ (p c524728 Var120))
||
||1. (~ (c (f522113 c524728 Var120 Var121) c524728))
||2. (p c524728 c524730)
||3. (pp c524728 c524730)
||4. (~ (p c524730 c524728))
||5. (~ (pp c524730 c524728))
||6. (~ (po c524730 c524728))
||7. (o c524730 c524728)
||8. (po c524729 c524728)
||9. (tpp c524730 c524729)
||
||> ((~ (p Y X)) <-- (po X Y))
||=============================
||Step 17
||
||? (po Var120 c524728)
||
||1. (p c524728 Var120)
||2. (~ (c (f522113 c524728 Var120 Var121) c524728))
||3. (p c524728 c524730)
||4. (pp c524728 c524730)
||5. (~ (p c524730 c524728))
||6. (~ (pp c524730 c524728))
||7. (~ (po c524730 c524728))
||8. (o c524730 c524728)
||9. (po c524729 c524728)
||10. (tpp c524730 c524729)
||
||> hyp
|=============================
|Step 18
|
|? (~ (c (f522113 c524728 c524729 Var121) c524730))
|
|1. (p c524728 c524730)
|2. (pp c524728 c524730)
|3. (~ (p c524730 c524728))
|4. (~ (pp c524730 c524728))
|5. (~ (po c524730 c524728))
|6. (o c524730 c524728)
|7. (po c524729 c524728)
|8. (tpp c524730 c524729)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 19
||
||? (p c524730 Var127)
||
||1. (c (f522113 c524728 c524729 Var121) c524730)
||2. (p c524728 c524730)
||3. (pp c524728 c524730)
||4. (~ (p c524730 c524728))
||5. (~ (pp c524730 c524728))
||6. (~ (po c524730 c524728))
||7. (o c524730 c524728)
||8. (po c524729 c524728)
||9. (tpp c524730 c524729)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 20
||
||? (pp c524730 Var127)
||
||1. (~ (p c524730 Var127))
||2. (c (f522113 c524728 c524729 Var121) c524730)
||3. (p c524728 c524730)
||4. (pp c524728 c524730)
||5. (~ (p c524730 c524728))
||6. (~ (pp c524730 c524728))
||7. (~ (po c524730 c524728))
||8. (o c524730 c524728)
||9. (po c524729 c524728)
||10. (tpp c524730 c524729)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 21
||
||? (tpp c524730 Var127)
||
||1. (~ (pp c524730 Var127))
||2. (~ (p c524730 Var127))
||3. (c (f522113 c524728 c524729 Var121) c524730)
||4. (p c524728 c524730)
||5. (pp c524728 c524730)
||6. (~ (p c524730 c524728))
||7. (~ (pp c524730 c524728))
||8. (~ (po c524730 c524728))
||9. (o c524730 c524728)
||10. (po c524729 c524728)
||11. (tpp c524730 c524729)
||
||> hyp
|=============================
|Step 22
|
|? (~ (c (f522113 c524728 c524729 Var121) c524729))
|
|1. (c (f522113 c524728 c524729 Var121) c524730)
|2. (p c524728 c524730)
|3. (pp c524728 c524730)
|4. (~ (p c524730 c524728))
|5. (~ (pp c524730 c524728))
|6. (~ (po c524730 c524728))
|7. (o c524730 c524728)
|8. (po c524729 c524728)
|9. (tpp c524730 c524729)
|
|> ((~ (c (f522113 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 23
|
|? (~ (p c524728 c524729))
|
|1. (c (f522113 c524728 c524729 Var121) c524729)
|2. (c (f522113 c524728 c524729 Var121) c524730)
|3. (p c524728 c524730)
|4. (pp c524728 c524730)
|5. (~ (p c524730 c524728))
|6. (~ (pp c524730 c524728))
|7. (~ (po c524730 c524728))
|8. (o c524730 c524728)
|9. (po c524729 c524728)
|10. (tpp c524730 c524729)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 24
|
|? (po c524729 c524728)
|
|1. (p c524728 c524729)
|2. (c (f522113 c524728 c524729 Var121) c524729)
|3. (c (f522113 c524728 c524729 Var121) c524730)
|4. (p c524728 c524730)
|5. (pp c524728 c524730)
|6. (~ (p c524730 c524728))
|7. (~ (pp c524730 c524728))
|8. (~ (po c524730 c524728))
|9. (o c524730 c524728)
|10. (po c524729 c524728)
|11. (tpp c524730 c524729)
|
|> hyp
=============================
Step 25

? (~ (p c524728 c524730))

1. (~ (pp c524730 c524728))
2. (~ (po c524730 c524728))
3. (o c524730 c524728)
4. (po c524729 c524728)
5. (tpp c524730 c524729)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 26
|
|? (c (f522113 c524728 Var144 Var145) c524728)
|
|1. (p c524728 c524730)
|2. (~ (pp c524730 c524728))
|3. (~ (po c524730 c524728))
|4. (o c524730 c524728)
|5. (po c524729 c524728)
|6. (tpp c524730 c524729)
|
|> ((c (f522113 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 27
|
|? (~ (p c524728 Var144))
|
|1. (~ (c (f522113 c524728 Var144 Var145) c524728))
|2. (p c524728 c524730)
|3. (~ (pp c524730 c524728))
|4. (~ (po c524730 c524728))
|5. (o c524730 c524728)
|6. (po c524729 c524728)
|7. (tpp c524730 c524729)
|
|> ((~ (p Y X)) <-- (po X Y))
|=============================
|Step 28
|
|? (po Var144 c524728)
|
|1. (p c524728 Var144)
|2. (~ (c (f522113 c524728 Var144 Var145) c524728))
|3. (p c524728 c524730)
|4. (~ (pp c524730 c524728))
|5. (~ (po c524730 c524728))
|6. (o c524730 c524728)
|7. (po c524729 c524728)
|8. (tpp c524730 c524729)
|
|> hyp
=============================
Step 29

? (~ (c (f522113 c524728 c524729 Var145) c524730))

1. (p c524728 c524730)
2. (~ (pp c524730 c524728))
3. (~ (po c524730 c524728))
4. (o c524730 c524728)
5. (po c524729 c524728)
6. (tpp c524730 c524729)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 30
|
|? (p c524730 Var151)
|
|1. (c (f522113 c524728 c524729 Var145) c524730)
|2. (p c524728 c524730)
|3. (~ (pp c524730 c524728))
|4. (~ (po c524730 c524728))
|5. (o c524730 c524728)
|6. (po c524729 c524728)
|7. (tpp c524730 c524729)
|
|> ((p Z X) <-- (~ (c (f522113 Z X Y) Z)))
|=============================
|Step 31
|
|? (~ (c (f522113 c524730 Var151 Var154) c524730))
|
|1. (~ (p c524730 Var151))
|2. (c (f522113 c524728 c524729 Var145) c524730)
|3. (p c524728 c524730)
|4. (~ (pp c524730 c524728))
|5. (~ (po c524730 c524728))
|6. (o c524730 c524728)
|7. (po c524729 c524728)
|8. (tpp c524730 c524729)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 32
||
||? (p c524730 Var157)
||
||1. (c (f522113 c524730 Var151 Var154) c524730)
||2. (~ (p c524730 Var151))
||3. (c (f522113 c524728 c524729 Var145) c524730)
||4. (p c524728 c524730)
||5. (~ (pp c524730 c524728))
||6. (~ (po c524730 c524728))
||7. (o c524730 c524728)
||8. (po c524729 c524728)
||9. (tpp c524730 c524729)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 33
||
||? (pp c524730 Var157)
||
||1. (~ (p c524730 Var157))
||2. (c (f522113 c524730 Var151 Var154) c524730)
||3. (~ (p c524730 Var151))
||4. (c (f522113 c524728 c524729 Var145) c524730)
||5. (p c524728 c524730)
||6. (~ (pp c524730 c524728))
||7. (~ (po c524730 c524728))
||8. (o c524730 c524728)
||9. (po c524729 c524728)
||10. (tpp c524730 c524729)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 34
||
||? (tpp c524730 Var157)
||
||1. (~ (pp c524730 Var157))
||2. (~ (p c524730 Var157))
||3. (c (f522113 c524730 Var151 Var154) c524730)
||4. (~ (p c524730 Var151))
||5. (c (f522113 c524728 c524729 Var145) c524730)
||6. (p c524728 c524730)
||7. (~ (pp c524730 c524728))
||8. (~ (po c524730 c524728))
||9. (o c524730 c524728)
||10. (po c524729 c524728)
||11. (tpp c524730 c524729)
||
||> hyp
|=============================
|Step 35
|
|? (~ (c (f522113 c524730 c524729 Var154) c524729))
|
|1. (c (f522113 c524730 c524729 Var154) c524730)
|2. (~ (p c524730 c524729))
|3. (c (f522113 c524728 c524729 Var145) c524730)
|4. (p c524728 c524730)
|5. (~ (pp c524730 c524728))
|6. (~ (po c524730 c524728))
|7. (o c524730 c524728)
|8. (po c524729 c524728)
|9. (tpp c524730 c524729)
|
|> ((~ (c (f522113 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 36
|
|? (~ (p c524730 c524729))
|
|1. (c (f522113 c524730 c524729 Var154) c524729)
|2. (c (f522113 c524730 c524729 Var154) c524730)
|3. (~ (p c524730 c524729))
|4. (c (f522113 c524728 c524729 Var145) c524730)
|5. (p c524728 c524730)
|6. (~ (pp c524730 c524728))
|7. (~ (po c524730 c524728))
|8. (o c524730 c524728)
|9. (po c524729 c524728)
|10. (tpp c524730 c524729)
|
|> hyp
=============================
Step 37

? (~ (c (f522113 c524728 c524729 Var145) c524729))

1. (c (f522113 c524728 c524729 Var145) c524730)
2. (p c524728 c524730)
3. (~ (pp c524730 c524728))
4. (~ (po c524730 c524728))
5. (o c524730 c524728)
6. (po c524729 c524728)
7. (tpp c524730 c524729)

> ((~ (c (f522113 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 38

? (~ (p c524728 c524729))

1. (c (f522113 c524728 c524729 Var145) c524729)
2. (c (f522113 c524728 c524729 Var145) c524730)
3. (p c524728 c524730)
4. (~ (pp c524730 c524728))
5. (~ (po c524730 c524728))
6. (o c524730 c524728)
7. (po c524729 c524728)
8. (tpp c524730 c524729)

> ((~ (p Y X)) <-- (po X Y))
=============================
Step 39

? (po c524729 c524728)

1. (p c524728 c524729)
2. (c (f522113 c524728 c524729 Var145) c524729)
3. (c (f522113 c524728 c524729 Var145) c524730)
4. (p c524728 c524730)
5. (~ (pp c524730 c524728))
6. (~ (po c524730 c524728))
7. (o c524730 c524728)
8. (po c524729 c524728)
9. (tpp c524730 c524729)

> hyp


LEMMA

split xz by dc/c; if c then ec/o; use the hard bridge on overlap; refine pp
=============================
Step 1

? (all x (all y (all z (((tpp x y) & (po y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (tpp c529494 c529493)) v (~ (po c529493 c529492))) v (((((dc c529494 c529492) v (ec c529494 c529492)) v (po c529494 c529492)) v (tpp c529494 c529492)) v (ntpp c529494 c529492)))


> hypdisj
=============================
Step 3

? (ntpp c529494 c529492)

1. (~ (tpp c529494 c529492))
2. (~ (po c529494 c529492))
3. (~ (ec c529494 c529492))
4. (~ (dc c529494 c529492))
5. (po c529493 c529492)
6. (tpp c529494 c529493)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c529494 c529492)
|
|1. (~ (ntpp c529494 c529492))
|2. (~ (tpp c529494 c529492))
|3. (~ (po c529494 c529492))
|4. (~ (ec c529494 c529492))
|5. (~ (dc c529494 c529492))
|6. (po c529493 c529492)
|7. (tpp c529494 c529493)
|
|> ((pp Y Z) <-- (tpp Y X) (po X Z) (o Y Z) (~ (po Y Z)))
||||=============================
||||Step 5
||||
||||? (tpp c529494 Var36)
||||
||||1. (~ (pp c529494 c529492))
||||2. (~ (ntpp c529494 c529492))
||||3. (~ (tpp c529494 c529492))
||||4. (~ (po c529494 c529492))
||||5. (~ (ec c529494 c529492))
||||6. (~ (dc c529494 c529492))
||||7. (po c529493 c529492)
||||8. (tpp c529494 c529493)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (po c529493 c529492)
|||
|||1. (~ (pp c529494 c529492))
|||2. (~ (ntpp c529494 c529492))
|||3. (~ (tpp c529494 c529492))
|||4. (~ (po c529494 c529492))
|||5. (~ (ec c529494 c529492))
|||6. (~ (dc c529494 c529492))
|||7. (po c529493 c529492)
|||8. (tpp c529494 c529493)
|||
|||> hyp
||=============================
||Step 7
||
||? (o c529494 c529492)
||
||1. (~ (pp c529494 c529492))
||2. (~ (ntpp c529494 c529492))
||3. (~ (tpp c529494 c529492))
||4. (~ (po c529494 c529492))
||5. (~ (ec c529494 c529492))
||6. (~ (dc c529494 c529492))
||7. (po c529493 c529492)
||8. (tpp c529494 c529493)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 8
|||
|||? (c c529494 c529492)
|||
|||1. (~ (o c529494 c529492))
|||2. (~ (pp c529494 c529492))
|||3. (~ (ntpp c529494 c529492))
|||4. (~ (tpp c529494 c529492))
|||5. (~ (po c529494 c529492))
|||6. (~ (ec c529494 c529492))
|||7. (~ (dc c529494 c529492))
|||8. (po c529493 c529492)
|||9. (tpp c529494 c529493)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 9
|||
|||? (~ (dc c529494 c529492))
|||
|||1. (~ (c c529494 c529492))
|||2. (~ (o c529494 c529492))
|||3. (~ (pp c529494 c529492))
|||4. (~ (ntpp c529494 c529492))
|||5. (~ (tpp c529494 c529492))
|||6. (~ (po c529494 c529492))
|||7. (~ (ec c529494 c529492))
|||8. (~ (dc c529494 c529492))
|||9. (po c529493 c529492)
|||10. (tpp c529494 c529493)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (ec c529494 c529492))
||
||1. (~ (o c529494 c529492))
||2. (~ (pp c529494 c529492))
||3. (~ (ntpp c529494 c529492))
||4. (~ (tpp c529494 c529492))
||5. (~ (po c529494 c529492))
||6. (~ (ec c529494 c529492))
||7. (~ (dc c529494 c529492))
||8. (po c529493 c529492)
||9. (tpp c529494 c529493)
||
||> hyp
|=============================
|Step 11
|
|? (~ (po c529494 c529492))
|
|1. (~ (pp c529494 c529492))
|2. (~ (ntpp c529494 c529492))
|3. (~ (tpp c529494 c529492))
|4. (~ (po c529494 c529492))
|5. (~ (ec c529494 c529492))
|6. (~ (dc c529494 c529492))
|7. (po c529493 c529492)
|8. (tpp c529494 c529493)
|
|> hyp
=============================
Step 12

? (~ (tpp c529494 c529492))

1. (~ (ntpp c529494 c529492))
2. (~ (tpp c529494 c529492))
3. (~ (po c529494 c529492))
4. (~ (ec c529494 c529492))
5. (~ (dc c529494 c529492))
6. (po c529493 c529492)
7. (tpp c529494 c529493)

> hyp
